A, B:Type, d:EqDecider(B). strong-subtype(A;B)  d  EqDecider(A) 

latex

Definitions	P & Q, P  Q, S  T, S  T, , P  Q, Prop, b, P  Q, EqDecider(T), x:A. B(x), strong-subtype(A;B), A & B, t  T
Lemmas	deq wf, strong-subtype wf, assert wf, iff wf, bool wf, rev implies wf